ISSN 1884-0760
GRACE TECHNICAL REPORTS
Guaranteeing Free-edits to Bidirectional
Graph Transformations
Ezgi C
¸ i¸cek
Soichiro Hidaka
GRACE-TR 2016–04
September 2016
CENTER FOR GLOBAL RESEARCH IN
ADVANCED SOFTWARE SCIENCE AND ENGINEERING
NATIONAL INSTITUTE OF INFORMATICS
2-1-2 HITOTSUBASHI, CHIYODA-KU, TOKYO, JAPAN
Guaranteeing Free-edits to Bidirectional Graph
Transformations
∗
Ezgi C
¸ i¸cek
MPI-SWS, Germany
[email protected]
Soichiro Hidaka
†Hosei University, Japan
[email protected]
Abstract
With recent advances in bidirectional graph transformations, changes to input and output graphs can be synchronized and both input and output graphs can be maintained consistently. However, in the previous work, the nature of supported input and output changes has been limited to in-place updates, whereas insertions and deletions have been handled by different mechanisms (such as universal resolving algorithm) that are costly and impractical. Motivated by this gap, we present a free-edit analysis to establish formal bidirectional properties to support free-edits (eg: deletions, insertions, in-place updates etc.) to a graph. With our approach, whenever free-edits are possible to a graph, the change can be directly reflected to the source without doing any backward evaluation. The key to our analysis is the utilization of correspondence traces that specify how a view edge is obtained. We prove our analysis sound with respect to the in-place update semantics and show that valid free-edits constitute a well-behaved bidirectional transformation. We implement the free-edit analysis and integrate it to the existing GRoundTram tool.
1
Introduction
Many applications operate on data that changes bidirectionally: view updates in a database are reflected to the corresponding source of the query [1, 6], changes to UML diagrams are incorporated to the source code or vice versa [18], meta data is kept consistently in two different formats with possible changes to both formats [9]. In all these applications, whenever the output is modified, the input should be updated consistently; and whenever the input is modified, the output should be updated consistently.
One way to ensure the consistency of information between input and output is to design programming languages that are bidirectional in nature. A program written in a bidirectional programming language specifies forward and backward transformations simultaneously and makes sure that consistency is preserved by construction. Bidirectional programs (transformations) are being widely used in different domains including the synchronization of replicated data in
∗The project was supported by the International Internship Program of the National
Institute of Informatics.
†Formerly of National Institute of Informatics, Japan
1 INTRODUCTION 2
different formats [8], view maintenance in relational databases [2], interactive user interface design [17], coupled software transformation [14] etc.
A complex data structure that is at the heart of many non-trivial bidi-rectional applications such as UML diagrams, biological information etc. is graphs. In their work, Hidakaet al. has proposed a framework to bidirection-alize graph transformations in which structural recursion is handled with bulk semantics [13]. Their work has developed a rigorous bidirectional semantics to ensure the correctness of backward and forward propagations for in-place updates.
Although the previous work has considered a wide range of graph edits, e.g. in-place updates, node/subgraph insertions and deletions, bulk of the bidirec-tional formalization has focused on providing well-behavedness and correctness guarantees for in-place updates. Unlike the in-place updates, graph edits such as insertions and deletions require non-uniform custom algorithms that might end up being inefficient and difficult to use. For instance, insertions to the view graph are handled in [13] by the universal resolving algorithm (URA) which tries to enumerate all possible subgraphs in the source that could have produced the updated view graph. In practice, this process is often costly since it requires enumerating and searching through all possibly inserted source subgraphs, and it gives little flexibility to the user to direct the enumeration process. Similarly, deletions to the view graph are handled in [13] by a correspondence based al-gorithm that require re-executing the forward evaluation from source to view to show correctness.
Even though these algorithms for handling insertions and deletions are cor-rect, they are often inefficient. In this work, we aim to design language-based techniques for efficient bidirectional propagation of arbitrary changes such as insertions, deletions or in-place updates. Our analysis on this direction relies on the fact that in practice, many queries just move parts of the data (i.e sub-graphs) around without inspecting the underlying input value. We observe that for parts of view graph which is obtained from the input data which is merely copied without being inspected, changes to the view graph can be directly re-flected to the source graph without doing any backward propagation, i.e. for the case of insertions, without invoking the costly URA algorithm, hence the name ’free’ and for the case of deletions, without requiring a forward evaluation to check the correctness. Similarly, for parts of the data that is not inspected, source changes can be directly reflected to the view graph without doing any forward propagation.
Therefore, we are interested in designing static techniques to identify whether free-edits to a graph (such as insertions, deletions, edge modifications, or arbitrary structural changes) are possible. As a first step in this direction, we design a proof system for establishing formal bidirectional properties to support free-edits to a graph for bidirectional programs written in the UnCAL language. In addition, we also ensure that free-edits preserve the well-behavedness properties.
2 FREE-EDIT ANALYSIS BY EXAMPLE 3
costly computation, we rely on the correspondence traces that specify how a view edge was obtained, and where it originates from in the source graph [11]. Initially, correspondence traces were developed for identifying the origin of a view edge and checking editability of a particular view edge without violating the well-behavedness properties. We observe that they are also useful for free-edit analysis.
A correspondence trace is defined as a list of code positions that ended in either an edge (if the view edge is originating from source graph) or a particular code position (if the view edge is originating from a constant label in the code). However, for edges that are originating from multiple code positions, e.g. resulting from union, lists do not suffice. In this work, we also lift traces from lists to sets for accommodating a more precise correspondence analysis and extend them further for structural recursion to also obtain which labels and variables contribute to the result. By utilizing an enhanced form of trace, we are able to identify whether free-edits are possible to a graph at a particular edit location in addition to obtaining a more precise origin and editability analysis. Thirdly, we also ensure that the WPutGet property holds for free-edits, i.e. the changes induced by backward evaluation followed by a forward evaluation also satisfy free-edit conditions.
Our proof system has a free-edit judgment of the form Γ ⊢ ep : b where
ep specifies the execution path for a specific edge ζ in the view graph and Γ specifies all the labels and variables occurring in the trace of the edit edgeζ. If the free-edit analysis succeeds, then the result of the analysisbis true (denoted as ⊤), else it is false (denoted as⊥).
In summary, we make the following contributions.
1. We develop a proof system for establishing bidirectional properties to sup-port free-edits to a graph and provide a cheap(free) backward propagation mechanism.
2. We show that the well-behavedness properties are preserved for any edit that passes our analysis.
3. We develop an enhanced form of correspondence traces to facilitate static proofs of free-edits.
4. We implement our analysis and integrate it into the existing GRoundTram tool and showcase the usefulness of our approach on several applications.
2
Free-edit Analysis by Example
Example 1 Suppose we have a program as shown in Listing 1 that extracts information for European countries from a source graph (shown in Fig. 1) that contains fact book information about different countries and their demographics. The resulting view graph is shown in Figure 2.
3 UNCAL: A CORE LANGUAGE FOR GRAPHS 4
select{result:{ethnic: $e, language: $lang, located: $cont}}
where{country:{name:$g, people:{ethnicGroup: $e}, language: $lang, continent: $cont}}in$db,
{$l:$Any}in$cont, $l= Europe
Listing 1: Transformation in UnQL
{&} 26 25 country 15 country 9 country 24 name 22 people 19 language 17 continent 23 Japan 21 ethnicGroup 20 Japanese 18 Japanese 16 Asia 14 name 12 people 3 continent 1 language 13 Germany 11 ethnicGroup 10 German 8 name 6 people continent language 7 Austria 5 ethnicGroup 4 Austrian 2 Europe 0 German
Figure 1: Example Source Graph {&} 0 13 result 14 result 3 language 7 located 10 ethnic 4 language 8 located 12 ethnic 1 German 2 German 5 Europe 6 Europe 9 Austrian 11 German
Figure 2: View Graph Gener-ated by Transformation of the Graph in Fig. 1
use because the user doesn’t have much control over the search strategy and can not specify the labels of the inserted graph. In addition, if the inserted subgraph is big, searching for a possible evaluation path that created the resulting view could be very inefficient due to an increase in the search space. Instead, using our proposed proof system, the user can determine whether free-edits are possible for a particular edit edge; in this caseζ. Since the graph variable $ecorresponding to the ethnicity information is not inspected, our analysis succeeds and we can directly reflect the insertion change to the source graph. To find where the new ethnicity information must be inserted in the source, we look up the origin edge of the edit edge ζ from its trace: the edge (12, ethnicGroup,11) is the origin. Hence, we insert the subgraph shown in Figure 3 next to the node (12, ethnicGroup,11).
3
UnCAL: A core language for Graphs
In this section, we first describe UnCAL (Unstructured CALculus), a powerful graph algebra [3] that is at the core of our development. We briefly explain the syntax and the evaluation semantics for vanilla UnCAL. Later on in Section 4, we extend UnCAL’s evaluation semantics with trace information to facilitate backward propagation.
We start with the semi-structured data shown in Figure 2 as a tree with
{&}
0 1
Turkish
3 UNCAL: A CORE LANGUAGE FOR GRAPHS 5
labelled edges and leaves. It contains the information about the result, e.g. language, location and ethnicity. This graph can be described in UnCAL’s syntax as shown below.
{result:{language:"Germany", located:"Europe", ethnic:"Austrian"}, result:{language:"Germany", located:"Europe", ethnic:"German"}}
Then, we can define functions (queries) in UnCAL to process the graph. For instance, a query that returns all countries can be defined in UnCAL by
rec(λ($l,$g).ifl= countrythen{country : $g}else{})($db)
The notation{· · · : · · ·,· · · } is used to represent graphs in UnCALs term language. The notation{t1,· · ·, tn}is used as an abbreviation of{t1} ∪ · · · ∪
{tn}.
UnCAL Graph Model An UnCAL graphs are directed and have (possibly multiple) root(s) and leaves. A graph is a quadruple (V, E, I, O), where V is a set of vertices (nodes),Eis a set of edges,Iis a one-to-one mapping from a set of input markers toV andOis a many-to-many mapping fromV to a set of output markers. A special marker &is called the default marker. If{&7→v} ∈I,v is
called an input node and ifv7→&m ∈O,vis called an output node. Intuitively,
input nodes serves entry points whereas the output nodes serve as exit points. The markers are used for references for cycles and sharings. Moreover, they are used as connection points to connect two graphs.
A dotted edge labelledϵis referred to as anϵ-edge, which is a virtual edge connecting two nodes directly. UnCAL’s notion of equality for graphs is modulo bisimulation (i.e., not modulo graph isomorphism).
UnCAL Query Language UnCAL’s term language consists of constants {},(), markers&y, definitions&x :=e, labelled edges{l:g}, vertical compositions g1@g2(append), horizontal compositionsg1⊕g2, other horizontal compositions
g1∪g2 for merging roots and cycles cycle(g). The underlying graph theoretic
meaning of these constructors are shown in Figure 4.
{} & ()
∅ &y &
&y
g ε ε cycle
g1
&x1...&xm
&x1...&xm &y1...&yn &x1...&xm
&y1...&yn
g1 g2 g1 g2
εε εε &x1 &xm&x1 &xm
&x1 &xm
∪
... ...
...
&y1 &ym′&y′1 &y′
n′
... ... &y1...&ym′&y′1...&y′n′ l
g1 g1
{_:_}
&
&
l
&y1...&ym &y1...&ym
&x :=
&x.&y1...&x.&ym
g1 g
&y1...&ym
...
&z1 &zn &z1...&zn
⊕
g1 g2
&x1...&xm&y1...&yn
g1 g2
&x1...&xm &y1...&yn
1 & &
m
x′… x′′&y1′…&yn′′ &x1′…&xm′′&y1′…&yn′′
ε ε
@
g1
&z1...&zk &x1 &xm
g2
... &y1 &yn
g1
... &x1 &xm
g2
... &y1 &yn
... ...
1 & &
m x′… x′′
1 & &
k z′… z′′ 1
& & m x′… x′′
Figure 4: Graph Constructors of UnCAL
4 BIDIRECTIONAL SEMANTICS 6
marker&) and no edges. The construct&y constructs a graph like{}, where the
node’s output marker is&y.
The remaining six constructors operate on other graphs. The constructor {l:g}constructs a new root with the default input marker&with an edgelfrom
the new root to the root of the graphg, i.e. g.I(&). The union constructorg1∪g2
operates on two graphs with identical sets of input markers and constructs new input nodes for each of the input markers of the graphs, where each new node is connected to the roots of g1 and g2 by ϵ edges. The vertical composition
constructg1@g2appends two graphs by connecting the output nodes ofg1to
the input nodes of g2byϵ edges. The rest of the markers ofg1 andg2that do
not match are ignored. The horizontal composition constructg1⊕g2unions two
graphs disjointly so that the resulting graph inherits all the markers, edges and nodes from the operands. The cycle constructioncycle(g) connects the output nodes ofg to the input nodes ofgbyϵedges to form cycles.
4
Bidirectional Semantics
In this section, we first describe a trace augmented forward and backward semantics for UnCAL (Section 4.1). We then prove our free-edit analysis sound relative to the backward semantics for three different kinds of edits: insertions, deletions, and edge label modifications (Section 6).
4.1
Traced Forward Semantics
We present a new trace-augmented forward semantics that is an extension of the original forward semantics presented in [13] and a variation of [11, 12]. The main extension that is motivated by [12] is that as a result of the forward execution, we also obtain a correspondence trace (similar to [12]) in addition to the resulting view graph. Correspondence traces keep track of code positions and source edges that directly contribute to the creation of each view edge (or respectively each node). In this paper, we make use of the traces for free-edit analysis unlike editability analysis conducted in [12].
The traced forward semanticsF[[e]]ρ= (g, t) evaluates an expressioneunder the environmentρand produces a view graphgand a tracet. The trace maps each view edge ∈ Edge to either a source edge (if it is originating from the source) or code position (if it is originating from the code), preceded by a set or a list of code positions representing the corresponding language constructs that created that particular view edge.
Trace = Edge→TraceE
TraceE ::=Pos::TraceE|[Edge]|[Pos]| {TraceE} |TraceE∪TraceE
The environmentρrepresents bindings for graph and label variables; it maps each graph variable to the corresponding input graph and each label variable to the corresponding label in the query.
Figure 5 shows the forward evaluation of each expression. We will focus on the trace component since the graph component is the same as in the original forward semantics of [13]. For the constructor {}p that creates a single node,
the trace maps the newly created node to the code positionpof the constructor. Similarly, the same trace is generated for the output marker constructor &y.
4 BIDIRECTIONAL SEMANTICS 7
F[[{}p]]
ρ= (G{}p,{G.I(&)7→[p]}) (T-emp)
F[[&yp]]
ρ= (G&yp,{G.I(&)7→[p]}) (Omrk)
F[[()p]]
ρ= (()p,∅) (G-emp)
F[[e1∪pe2]]ρ= (G(g1∪pg2),(t1∪t2∪{v7→[p]|(&x 7→v)∈G.I}))
where ((g1, t1),(g2, t2)) = (F[[e1]]ρ,F[[e2]]ρ)
(Uni) F[[e1⊕pe2]]ρ= (g1⊕pg2, t1∪t2)
where ((g1, t1),(g2, t2)) = (F[[e1]]ρ,F[[e2]]ρ)
(Duni) F[[e1@pe2]]ρ= (g1@pg2, t1∪t2)
where ((g1, t1),(g2, t2)) = (F[[e1]]ρ,F[[e2]]ρ)
(Apnd) F[[{eL :e}p]]ρ= (G{l:g}p,{(G.I(&), l, g.I(&))7→τ, G.I(&)7→[p]}∪t)
where ((l, τ),(g, t)) = (FL[[eL]]ρ,F[[e]]ρ)
(Edg) F[[(&x :=e)p]]
ρ= (&x :=g, t)
where (g, t) =F[[e]]ρ
(Imrk)
F[[cyclep(e)]]
ρ= (Gcycle
p(g), t∪{v7→[p]|(&x 7→v)∈G.I})
where (g, t) =F[[e]]ρ
(Cyc) FL[[ap]]ρ= (a,[p]) (Lcnst)
FL[[$lp]]ρ= (l,[p])
wherel=ρ($l)
(Lvar)
F[[lletp $l =eLine]]ρ= (g, t◦$l (p:τ))
where(l, τ) =FL[[eL]]ρ
where(g, t) =F[[e]]ρ∪{$l7→l}
(Llet)
F[[letp $g =e1ine2]]ρ= (g2, t2◦$g(preppt1))
where(g1, t1) =F[[e1]]ρ
where(g2, t2) =F[[e2]]ρ∪{$g7→g1}
(Let)
F[[$gp]]
ρ= (g,prepp⌜g⌝)
where g=ρ($g)
(Var)
F[[if
p(e
L=e′L)thenetrue
else efalse]]ρ= (g,preppt)
where((l, ),(l′, )) = (FL[[eL]],FL[[e′L]])
b= (l=l′)
(g, t) =F[[eb]]ρ
(If)
4 BIDIRECTIONAL SEMANTICS 8
F[[recpZ(λ($l,$g).eb)(ea)]]ρ= (g′, ∪
ζ∈g.E
tζ∪t′V)
where(g, t) =F[[ea]]ρ
M ={ζ7→(gm, t′′m)|ζ∈g.E, ζ̸=ε,(u, l, v) =ζ,
(gm, tm) =F[[eb]]ρ∪{$l7→l,$g7→gv},
t′
m= (tm◦$l(p:t(ζ))◦$g(prepptv)),
∀ζm∈gm. iforigin(ζm, tm)∈ga.Top
thent′′
m=prep$lt′m
elset′′
m=t′m}
g′= (V
RecN∪. . . , , , ) =composeprec(M, g,Z)
t′
V ={v7→[p]|v∈VRecN}
tζ =recep,ζ(preppπ2(M(ζ)))
(Rec)
generated since there is no edge or node created. For the binary constructors ∪, ⊕ and @, the traces of both subexpressions are merged together with the trace created by themselves. The merging of tracest1∪t2is computed as follows:
{ζ7→(if(ζ7→τ2)∈t2 thenτ1∪τ2 elseτ1)| (ζ7→τ1)∈t1} ∪
{ζ7→τ2 | (ζ7→τ2)∈t2∧(ζ7→τ1)∈/t1}
If the view edge ζ is originating from only one of the operands, then we return the corresponding trace edge set. It might also be the case that the view edge is originating from both of the operands (i.e.ζ ∈dom(t1)∧ζ∈dom(t2)).
For instance the query rec((λ$l,$g).$gp1∪$gp2) will create a subgraph which
is shared and any edge in this subgraph will be originating from both p1 and
p2 code locations with an identical origin edge. In such cases, we simply union
their corresponding trace edge sets τ1 andτ2.
Next, we define what we mean by the origin of a view edge. The edge origin originEis defined by
originE(p::τ) =originE(τ)
originE([x]) =xwherex∈(Edge| Pos)
originE({τ1, τ2,· · ·, τN}) =originE(τ1) where∀i.originE(τ1) =originE(τi).
Note thatτ1∪τ2 is defined only if the view edge has the same origin edge,
that is originE(τ1) =originE(τ2).
For the remaining binary graph constructors ⊕ and @, the traces of both subexpressions are combined together with the trace created by themselves.
For variables, we return the identity trace that maps each edge (resp. each node) in the graph to itself.
Label evaluation is denoted asFL[[el]]ρ, taking as input a label expressions
eL and an environmentρ, and returning a label and a corresponding trace. If
the label expression is a constant, then the trace is simply the code position of the label (rule Lconst). If the label expression is a label variable, then the trace is the code position of the label variable followed by the corresponding trace of the variable from the environment.
For the let bindings of the form lletp $l = eL in e, we first evaluate the
5 FREE-EDIT ANALYSIS 9
environment mappingl to the result of the label evaluation. The trace for the whole let expression does not only contain the trace of the body, but also the trace of the bind expression as well as the code location of the let expression. This composition is represented by a substitution operation, denoted ast1◦$lt2,
that substitutes the trace oft1for all the edges originating from the label variable
l in the trace of the body expression. The aim of this substitution is to create a final trace for the whole let expression that encapsulates all the information contained in eL and e. Let bindings for the graph variables follow a similar
pattern.
Our forward semantics is a variation of the trace-augmented forward seman-tics developed in [11], with two important differences: 1) traces are not merely lists, but are also sets and 2) the environment for the forward evaluation doesn’t store the trace information for each binding. Therefore, the initial environment
ρ0just maps the distinct graph variable $dbto the initial graphgs. The
advan-tage of having a more complex type for traces is that it allows us to have more precise information for union operations. For instance, consider the following program let$g ={a: $dbp1
} in{b : $gp2} ∪ {c : $dbp3
} and the view edge ζ
that originates from the input graph bound to $db. According to the seman-tics proposed in [11], the traces are lists, and for union operation, union of the traces is not well-defined if the view edge originates from both components; it only stores the code locations of one of the operands, not both. To gain back the precision for such cases, we allow traces to be also sets. Then, for view edge
ζ, the trace will store bothp2and p3 as well asp1.
Coincidence Our forward semantics coincides with the forward semantics developed in [11] as long as the environments are identity-preserving, i.e. the initial environment given to the forward semantics of [11] simply maps the graph variable $db to the input graph without recording any additional trace information.
5
Free-edit analysis
Initially, we assume that after forward-execution of the expression e under an input environmentρ, we obtain a resulting graphGand a corresponding trace
t. Given this trace, we assume that user selects an edgeζin the resulting graph
G. Free-edit analysis consists of three steps.
In the first step, given an edit edge ζ in the resulting graphG, we extract the execution path of the expression e that resulted in the selected edit edge. This extraction mechanism, denoted asextract(t, e, ζ), is defined by a recursive procedure, shown in Figure 7. The aim of the extraction phase is to eliminate parts of the expression that are irrelevant for the free-edit analysis. The syntax of execution paths is a subset of the syntax of expressions: the only difference is that execution paths do not contain conditional expressions. For instance, consider the expression ifp(eL = eL′ ) then etrue else efalse. If the resulting
edge is originating from thethen branch, the extracted execution path would only contain the execution path corresponding toetrue whereasefalse is simply
omitted.
5 FREE-EDIT ANALYSIS 10
Γ⊢e:b execution pathe
$g∈Γ
Γ⊢$g:⊤ GVAR Γ⊢$l:⊥ LVAR Γ⊢ {}p
,&yp
,()p
:⊥ CONST
FLV(l1, l2)∩Γ =∅ Γ⊢e:b Γ⊢ewith(l1=l2) :b
IF el̸∈Γ Γ⊢e:b
Γ⊢ {el:e}p:b EDG
Γ⊢e:b
Γ⊢(&x :=e)p:
b IMRK
Γ⊢eg:⊤ Γ⊢e:b $g ∈Γ
Γ⊢letp$
g=eg ine:b
LET1
Γ⊢eg:⊥ Γ⊢e:b $g∈/Γ Γ⊢letp
$g =egine:b
LET2 Γ⊢e:b $l∈/Γ
Γ⊢lletp
$l=eLine:b LLET
Γ⊢ea:⊤ Γ⊢eb:⊤ $l∈/Γ $g ∈Γ
Γ⊢recp
Z (λ($l,$g).eb)(ea) :⊤
REC1
Γ⊢ea:⊥ Γ⊢eb:b {$g,$l}∈/Γ Γ⊢recp
Z (λ($l,$g).eb)(ea) :b
REC2 Γ⊢e1 :b1 Γ⊢e2:b2
Γ⊢e1∪pe2:b1∨b2 UNI
Γ⊢e:b
Γ⊢cyclep
(e) :b CYC
Figure 6: Analysis rules
referred as the origin set. Intuitively, Γ contains the origin label variables and constants in the expression e that contributed to the creation of the selected edgeζ.
Finally, in the third step, we perform the actual free-edit analysis given the execution path e and the origin set Γ. Our analysis abstracts over the edge, it only requires the origin set (Γ) and the execution path (e). The analysis judgment Γ⊢e:bspecifies whether free-edits for the execution patheand the origin set Γ are possible. If so, the analysis succeeds, i.e. the result is⊤. If not, the analysis fails, i.e. the result is ⊥.
Figure 6 represents the analysis rules for determining whether free-edits are possible. The main principle behind the rules is that analysis fails whenever a label variable or a constant is in the origin set, i.e. it might be possibly inspected. We explain each of the rules in detail. The rule GVAR succeeds whenever graph variable $g is in the origin set Γ, i.e. the edge is originating from part of the graph that is directly copied. The rule LVAR immediately fails for any label variable. Our analysis conservatively rejects free-edits to label vari-ables due to two main reasons: 1) their modification might require backward propagation due to a possibly different execution path and 2) insertions/dele-tions of subgraphs at the selected edge correspond to inserting/deleting parts of the original expression. The latter is a modification that is not allowed in bidirectional transformations.
5 FREE-EDIT ANALYSIS 11
extract(t,{}p, ζ) ={} (E-T-emp)
extract(t,&yp, ζ) =&y (E-Omrk)
extract(t,()p, ζ) = () (E-G-emp)
extract(t1∪t2∪t′, e1∪pe2, ζ) =extract(t1, e1, ζ)∪extract(t2, e2, ζ)
where ζ∈dom(t1)∧ζ∈dom(t2)
(E-Uni-1) extract(t1∪t2∪t′, e1∪pe2, ζ) =extract(t1, e1, ζ)
where ζ∈dom(t1)∧ζ /∈dom(t2)
(E-Uni-2) extract(t1∪t2∪t′, e1∪pe2, ζ) =extract(t2, e2, ζ)
where ζ /∈dom(t1)∧ζ /∈dom(t2)
(E-Uni-3)
extract(t1∪t2, e1⊕pe2, ζ) =extract(t1, e1, ζ)⊕extract(t2, e2, ζ)
(E-Duni)
extract(t1∪t2, e1@pe2, ζ) =extract(t1, e1, ζ) @extract(t2, e2, ζ)
(E-Apnd) extract(t∪t′,{eL:e}p, ζ) ={eL:extract(t′, e, ζ)}
(E-Edg) extract(t,(&x:=e)p, ζ) = (&x :=extract(t, e, ζ))
(E-Imrk) extract(t∪t′,cyclep(e), ζ) =cycle(extract(t, e, ζ))
(E-Cyc)
extract(t,ap, ζ) =a (E-Lcnst)
extract(t,$lp, ζ) = $l (E-Lvar)
extract(t◦$l(p:τ),lletp $l =eL ine, ζ) =lletp $l=eLinextract(t, e, ζ)
(E-LLet)
extract(t2◦$g(preppt1),letp $g=e1ine2, ζ) =letp $g=extract(t1, e1,origin(t2, ζ))in
extract(t2, e2, ζ)
where $g occurs int2
(E-Let1) extract(t2◦$g(preppt1),letp $g=e1ine2, ζ) =extract(t2, e2, ζ)
where $g not occurs int2
(E-Let2)
extract(t,$gp, ζ) = $g (E-Gvar)
extract(prep
p,b
t,if
p(e
L=e′L)thenetrue
else efalse, ζ) =extract(t, eb, ζ) (
E-If)
extract( ∪
ζ∈g.E
tζ ∪t′V,
p
rec
Z (λ($l,$g).eb)(ea), ζ) =rec(λ($l,$g).eb)(ea)
where $g occurs intζ
(E-Rec)
6 METATHEORY 12
of the body succeeds. The rule EDG succeeds only if the analyzed edge is not originating from the selected edge. The rule IMRK succeeds only if the analysis of the renamed graph succeeds. Rules LET1 and LET2 represent two cases for the analysis of the let construct for graph variables. If the bound variable $g
is in the origin set, then analysis succeeds if analysis of both of the body and the argument expressions succeed (rule LET1). If the bound variable $g is not in the origin set, then it suffices for only the analysis of the body expression to succeed (rule LET2). The rule LLET represent the analysis of the let construct for label variables. It succeeds only if the bound label is not in the origin set and the body expression’s analysis succeeds.
Similar to let construct for graph variables, there are two cases for therec
construct. If the graph variable $g, but not the label variable $l, is in the origin set, then analysis succeeds if analyses of both of the body and the argument expressions succeed (rule LET1). If none of the the graph variable $g and the label variable $l are in the origin set, then it suffices for only the analysis of the body expression to succeed. The rule UNI succeeds if any one of the analyses of the operands of the union succeed. Finally, the rule CYC succeeds if the analysis of the body of the cycle construct succeed.
6
Metatheory
In this section, we first show the equivalence of our forward semantics to the one developed in [11] modulo the problem mentioned with respect to unions. Then, we show the soundness of our analysis, i.e. whenever our analysis succeeds, it is indeed possible to directly reflect the changes at the selected edge to the origin without actually performing any backward propagation. In addition, we show that any change that passes our analysis also satisfies the WPutGet property.
We denote the forward semantics developed in [11] as F[[·]]·. An identity environment is the one that takes the distinct graph variable $db to the corre-sponding input graph.
Lemma 1 (Equivalence of Forward Semantics)
Let ρ be the identity environment and ρ′ be the arbitrary environment, then
F[[e]]ρ∪ρ′ = (g, t) ⇐⇒ F[[e]]ρ∪π1ρ′ = (g, t◦$x1 · · · ◦$xn π2(ρ
′($x
n))) where
dom(ρ′) ={$x
1,· · · ,$xn}.
The coincidence of the two forward semantics follows as a corollary of this equivalence lemma whenever the initial envrironment is the identity environ-ment.
Corollary 2 (Coincidence)
Ifρ0 is the identity environment, thenF[[e]]ρ0=F[[e]]π1(ρ0).
Proof. This follows immediately by Lemma 1.
Theorem 3 (Soundness Equivalence Simplified)
LetF[[e]]ρ0 = (G, t) andζ∈G.Edgesbe the location user wants to edit.
Assume e′=extract(e, t, ζ) andFLV(t(ζ))⊆Γ.
If Γ⊢e′:⊤, then for any updateupd(G, ζ) =G′, we have
B[[e]]ρ0G
′=prop(ρ
7 RELATED WORK 13
Theorem 4 (Main Soundness Theorem)
LetF[[e]]ρ0 = (G, t) andζ∈G.Edgesbe the location user wants to edit. Letζibe the set of edges that are created by the same applied edge asζ.
Assume e′ =extract(t, ζ, e) ande′
i =extract(e, t, ζi) and FLV(t(ζ))⊆Γ and
FLV(t(ζi))⊆Γi.
If Γ⊢e′:⊤and Γ
i⊢e′i:⊤, then for any updateupd(G, ζ) =G′, we have
B[[e]]ρ0G
′=prop(ρ
0,upd, ζ, t) and the WPutGet will be satisfied.
Origin LetF[[e]]ρ = (g, t). For an edge ζ ∈g, its origin is defined as a pair (p, ζ′) wheret(ζ′) = [· · ·p ζ′].
Update Propagation Assume that F[[e]]ρ = (g, t). Then, for an edge
ζ ∈ g, update propagation is defined as prop(ρ,upd, ζ, t) = {ρ[$x ← upd(G, ζ′)]|($x, ζ′) =origin(ζ, t) ∧G=ρ($x) ∧ζ′ ∈G.Edges}
7
Related Work
The notion of provenance – information about the origin, derivation, ownership, or history of an object [4] – is extensively studied in the database community and many other application fields [5]. Why (lineage), how and where provenance are computed using linguistic approach in a homomorphic manner where the mathematical structure of the trace is preserved during the computation of the queries. Present work also rely on trace information to accommodate not only label renaming but also deletion and insertion, by identifying the region in the view that accepts free edits.
Though database community exploits provenance information in the con-text of backward transformation like the work by Fegaras [7], perhaps the most closely related work to ours is semantic bidirectionalization [19] that generates correspondences between input and output elements over polymorphic trans-formations by feeding to the forward transformation the “artificial” data that includes location identifiers for each element instead of the actual elements. Re-sulting location information appears in the view corresponds to our traces when they are originated from source. Since we deal with graphs, we combine two traces using directed acyclic graph, so the trace is more enriched in our setting. Voigtlaender’s approach benefits from semantic approach in which the forward transformation can be described in any general purpose language, whereas we use syntactic information of a domain (graph transformation) specific language UnCAL.
Our transformations are monomorphic as opposed to the Voigtlaender’s setting, because we have transformations including conditionals that compares label variables with label constants. Matsuda and Wang [15, 16] tackled this problems by run-time recording of control flow to be able to check and reject the control flow change during the backward transformation.
REFERENCES 14
general approach in the programming language field, but we do not have clear road map for this yet.
Acknowledgments
The project was supported by the International Internship Program of the National Institute of Informatics. The authors would like to thank the IPL members for their valuable comments during the internship period.
References
[1] Fran¸cois Bancilhon and Nicolas Spyratos. Update semantics of relational views. ACM Trans. Database Syst., 6(4):557–575, 1981.
[2] Aaron Bohannon, Benjamin C. Pierce, and Jeffrey A. Vaughan. Relational lenses: a language for updatable views. In PODS 2006, pages 338–347, 2006.
[3] Peter Buneman, Mary Fernandez, and Dan Suciu. UnQL: a query language and algebra for semistructured data based on structural recursion. The VLDB Journal, 9(1):76–110, 2000.
[4] James Cheney, Umut A. Acar, and Amal Ahmed. Provenance traces.
CoRR, abs/0812.0564, 2008.
[5] James Cheney, Laura Chiticariu, and Wang-Chiew Tan. Provenance in databases: Why, how, and where. Foundations and Trends in Databases, 1(4):379–474, 2009.
[6] Umeshwar Dayal and Philip A. Bernstein. On the correct translation of update operations on relational views. ACM Trans. Database Syst., 7(3):381–416, 1982.
[7] Leonidas Fegaras. Propagating updates through xml views using lineage tracing. InICDE 2010, pages 309–320, 2010.
[8] J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bi-directional tree transforma-tions: a linguistic approach to the view update problem. In POPL 2005, pages 233–246, 2005.
[9] John Grundy, John Hosking, and Warwick B. Mugridge. Inconsistency management for multiple-view software development environments. IEEE Trans. Softw. Eng., 24(11):960–981, 1998.
[10] Makoto Hamana. Iteration algebras for unql graphs and completeness for bisimulation. In Proceedings Tenth International Workshop on Fixed Points in Computer Science, FICS 2015, Berlin, Germany, September 11-12, 2015., pages 75–89, 2015.
REFERENCES 15
[12] Soichiro Hidaka, Martin Billes, and Quang Minh Tran. Trace-based ap-proach to editability and correspondence analysis for bidirectional graph transformations. InFourth International Workshop on Bidirectional Trans-formations (Bx 2015), 2015.
[13] Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, and Keisuke Nakano. Bidirectionalizing graph transformations. InICFP’10, pages 205–216. ACM, 2010.
[14] Ralf L¨ammel. Coupled Software Transformations (Extended Abstract). In First International Workshop on Software Evolution Transformations (SET 2004), pages 31–35, November 2004.
[15] Kazutaka Matsuda and Meng Wang. Bidirectionalization for free with run-time recording: Or, a light-weight approach to the view-update problem. InProceedings of the 15th Symposium on Principles and Practice of Declar-ative Programming, PPDP ’13, pages 297–308, New York, NY, USA, 2013. ACM.
[16] Kazutaka Matsuda and Meng Wang. “bidirectionalization for free” for monomorphic transformations.Science of Computer Programming, 111:79– 109, 2015. DOI:10.1016/j.scico.2014.07.008.
[17] Lambert Meertens. Designing constraint maintainers for user interaction. http://www.kestrel.edu/home/people/meertens/, June 1998.
[18] Perdita Stevens. Bidirectional model transformations in QVT: semantic issues and open questions.Software and System Modeling, 9(1):7–20, 2010.
